COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	circum[e87,jmc]		Yet another approach to circumscription
C00006 ENDMK
C⊗;
circum[e87,jmc]		Yet another approach to circumscription

Introduce a function from models of the axioms to an ordered domain
and choose models that minimize this function.  The function is
called the  abnormality  function.  In the proof-theoretic version
of this kind of abnormality theory, enough is reified and enough
predicates and functions are available so that this
function and the ordering of the abnormality
domain are described by functions involving
the substantive predicates and functions of the language being used.
The ordered domain, call it  AB, will most likely be a function space
and its ordering will be derived from orderings on the domain
and range of the function.

examples and wanted examples

1. Minimizing  isblock.  This example, readily done, by the simplest
form of circumscription isn't what we want the new theory for, but
it had better be doable.

ab(isblock,p,f,g) = λx.isblock x.

Here we are supposing that there may be some additional predicates
and functions in the theory and axioms connecting them with  isblock.

Hmm. How do we say that  p  and  f  are variable, and  g  is not?

Looks like  ab(isblock,p,f;g)  will do it.

2. birds and flying including canaries.

In predicate calculus there is a fundamental difference between
parametrizing what's in the domain and what domain elements the
predicates apply to.  In a set theory formulation, we may be
able to treat the two more uniformly.

In the  flying  example, even in the most elaborate cases so far
studied, the minimization is performed separately for each object  x,
i.e. it's essentially propositional.

ab = foo(¬feathered, canary ∧ ¬bird, bird ∧ ¬flies, ostrich ∧ flies,
	flies)

where  foo  is a suitable function that makes boolean vectors out
of boolean variables.  It looks like if we do this correctly we
can use the usual parallel ordering on boolean vectors.

priority(p,q) = (p∧q,p,p∨q)

Suppose we also have  u+v, means concatenating the boolean vectors
u  and  v.

Vladimir points out that if we regard  p,  q,  etc.  as the binary
digits of a number, the total ordering among,  p,  q,  etc.  is
just the ordering of the numbers.  For generality, we would need
to be able to combine numbers, whose digits are only partially
ordered.